|
| creator |
Horsch, Martin Thomas
| | date |
2006-06-07
| | | | description |
130 pages
| |
Temporal logics are a widespread formalism for the specification of
the behaviour exhibited by a system in the course of time. Kamp
proved that, if this behaviour is modeled as a sequence of actions,
the approach known as linear temporal logic can express the same
properties as first-order logic.
When a model represents a distributed system it is desirable to
formalize the temporal dependence between its actions as a partial
rather than a linear order. Mazurkiewicz traces are an extension of
words by the partial commutation $ab = ba$ for certain letters of
the alphabet. There are two different approaches which generalize
linear temporal logic to Mazurkiewicz traces while preserving its
completeness with respect to first-order logic: local temporal
logic, which expresses properties from the perspective of single
elements of a partial order, and a global approach that can be used
to describe states of the system as a whole.
This text presents both approaches, with an emphasis on fragments of
the local temporal logic, which are also compared to fragments of
first-order logic. All results are obtained with the use of
Ehrenfeucht-Fraisse games. These are simple and deterministic
non-cooperative games with two players who can place pebbles on the
vertices of two traces. The rules are chosen such that a winning
strategy for one of the players corresponds to the existence of a
logical formula which assumes different truth values for these
traces.
--
Temporallogiken sind ein weit verbreiteter Formalismus für die
Spezifikation des zeitlichen Verhaltens eines Systems. Falls dieses
Verhalten als eine Sequenz von Aktionen dargestellt wird, kann man
nach einem Satz von Kamp mit der Linearzeitlogik LTL die gleichen
Eigenschaften ausdrücken wie in der Logik erster Stufe.
Für die Modellierung eines verteilten Systems ist es sinnvoll, die
zeitliche Abfolge seiner Aktionen als Partialordnung statt als
lineare Ordnung darzustellen. Mazurkiewicz-Spuren sind eine
Erweiterung von Wörtern um die partielle Kommutativität ab = ba
für bestimmte Buchstaben aus dem Alphabet. Zwei verschiedene
Ansätze verallgemeinern LTL auf Mazurkiewicz-Spuren und erhalten
dabei die Vollständigkeit in Bezug auf die Logik erster Stufe: zum
einen die lokale Temporallogik, die Eigenschaften aus der
Perspektive einzelner Elemente der Partialordnung formuliert, und
zum anderen die globale Linearzeitlogik, die Zustände des
Gesamtsystems beschreibt.
Dieser Text stellt die beiden Ansätze vor. Der Schwerpunkt liegt
auf der Untersuchung von Fragmenten der lokalen Temporallogik, die
auch mit Fragmenten der Logik erster Stufe verglichen werden. Alle
Ergebnisse werden mit Ehrenfeucht-Fraisse-Spielen bewiesen. Dabei
handelt es sich um einfache und deterministische nichtkooperative
Spiele, in denen Marken von zwei Spielern auf die Knoten zweier
Spuren gesetzt werden. Die Regeln werden so gewählt, dass eine
Gewinnstrategie für einen dieser Spieler der Existenz einer Formel
entspricht, die für die beiden Spuren unterschiedliche
Wahrheitswerte annimmt.
| | format |
application/pdf
| | 2205790 Bytes | |